A:MsgA, x, z:Id, k:Knd, s1, s2:A.(timed)state, v:A.da(k).
ma-frame-compat(A;A)
 (A.rframe(k reads x))
 ma-x-tequiv(A;x;s1;s2)
 ((z = x))
 (A.ef(k,z,read-state(s1),v)?s1(z) = A.ef(k,z,read-state(s2),v)?s2(z)  A.ds(z)) 

latex

Definitions

f(a), <a, b>, , Id, Type, Top, f(x)?z, x:AB(x), s = t, x:A. B(x), P & Q, Knd, x:A  B(x), t.1, t.2, Void, f(x), b, A, b, , , x.A(x), x. t(x), IdDeq, KindDeq, a:A fp B(a), product-deq(A;B;a;b), x  dom(f), P  Q, P  Q, Unit, left + right, M.ef(k,x,s,v)?w, State(ds), timedState(ds), xdom(f). v=f(x)   P(x;v), M.da(a), z != f(x)  P(a;z), M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), M.ds(x), ma-x-tequiv(M;x;s1;s2), Valtype(da;k), M.(timed)state, M.rframe(k reads x), MsgA, read-state(s), (s1  s2 mod x), M.state, t  T, x:A.B(x), Atom$n, inl x , case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , type List, False, P  Q, S  T, Dec(P), IdLnk, suptype(S; T), s ~ t, {T}, SQType(T)

Lemmas

fpf-ap wf, fpf-cap-void-subtype, decidable assert, ma-x-tequiv wf, ma-rframe wf, ma-frame-compat wf, ma-da wf, ma-tst wf, msga wf, read-state wf, ma-x-equiv-read-state, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, product-deq wf, fpf-trivial-subtype-top, Kind-deq wf, pi1 wf, top wf, rationals wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, Id wf, bool wf, bnot wf, not wf, assert wf